a, b:. ((a = 0  )  (b = 0  )  (0 < a & 0 < b)  (0 < -(a) & 0 < -(b)))  0  a * b 

latex

Definitions	{T}, T, (i = j), qeq(r;s), ff, i <z j, tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.2, t.1, , x f y, if b then t else f fi , b, a  b, r * s, r  s, True, , t  T, P  Q, P  Q, P & Q, P  Q, P  Q, x:A. B(x), False, A, Dec(P), S  T
Lemmas	qmul-zero, qless complement qorder, qless trichot qorder, decidable equal rationals, qle weakening lt qorder, qmul-positive, qmul zero qrng, true wf, squash wf, qle wf, qmul wf, qless wf, int inc rationals, rationals wf